f  g == x:A. x  dom(f)  x  dom(g) & f(x) = g(x) 

latex

---

clarification:

fpf-sub(A; a.B(a); eq; f; g)
== x:A. fpf-dom(eq; x; f)  fpf-dom(eq; x; g) & fpf-ap(f; eq; x) = fpf-ap(g; eq; x)  B(x) 

latex

Definitions	x:A. B(x), P  Q, A & B, b, x  dom(f), f(x)
FDL editor aliases	fpf-sub